/*
	階層の導入
*/

module tour/addressBook4

abstract sig Target {}

// 名前
abstract sig Name extends Target {}

// アドレス
sig Addr extends Target {}

// エイリアス
sig Alias, Group extends Name {}

// アドレス帳
sig Book { 
	names: set Name, 
	addr: names -> Target
}
{
	// 自分自身から到達可能なターゲットに自分自身が含まれる名前は存在しない
	no n: Name | n in n.^(addr)

	// 別名が持つターゲットは最大１つ
	all a: Alias | lone a.addr
}

// 表示
pred show (b: Book) {
	some Alias.(b.addr)
}
run show for 3 but 1 Book

// アドレス帳にアドレスを追加する操作
pred add (b, b': Book, n: Name, t: Target) {
	b'.addr = b.addr + n -> t
}
run add for 3 but 2 Book

// 削除する述語
pred del (b, b': Book, n: Name, t: Target) {
	b'.addr = b.addr - n -> t
}

// 参照する関数
fun lookup(b: Book, n: Name) : set Addr {
	n.^(b.addr) & Addr
}

// 名称に紐づくアドレスが必ずいくつか見つかることを確認する
assert lookupYields { 
	all b: Book, n: b.names | some lookup [b, n]
}

// 削除処理は追加操作のアンドゥであることを確認。
assert delUndoAdd {
	all b, b', b'': Book, n: Name, t: Target |
		no n.(b.addr) and add[b, b', n, t] and del[b', b'', n, t] implies b.addr = b''.addr
}

// 追加を繰り返しても変化がない
assert addIdempotent { 
	all b, b', b'': Book, n: Name, t: Target |
		add[b, b', n, t] and add[b', b'', n, t] implies b'.addr = b''.addr
}

// 追加をした場合に追加した名称以外のアドレスには影響ないことを確認する
assert addLocal {
	all b,b': Book, n,n': Name, t: Target |
		add[b, b', n, t] and n != n' implies lookup[b, n'] = lookup[b', n']
} 

check lookupYields for 4 but 1 Book
check addIdempotent for 3
check delUndoAdd for 10 but 3 Book
check addLocal for 10 but 3 Book
